Skip to content

Docs(13962): consolider le scan junctions po-2025 dans la doc existante -- 3e cecite d'instrument - #19860

Merged
myia-ai-01 merged 6 commits into
mainfrom
docs/13962-junctions-scan-po-2025
Oct 9, 2026
Merged

myia-ai-01 merged 6 commits into
mainfrom
docs/13962-junctions-scan-po-2025

Conversation

@jsboige

@jsboige jsboige commented Oct 8, 2026 •

Copy link
Copy Markdown
Owner

Grain: MED/docs — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #19620

Reprise de la CR 5463024284 (ai-01, 2026-10-08)

La v1 de cette PR déposait docs/lean/junctions-scan-po-2025.md — un rapport de scan de machine daté. La CR l'a refusée : CLAUDE.md §A et harness-hygiene interdisent les rapports de cycle/audit dans le dépôt. Reprise en deux temps, sans perte :

  1. Préservation intégrale AVANT retrait : la mesure complète (verdict, tableaux, scan verbatim, share-state, protocole, position flotte) est posée sur le dashboard RooSync workspace-CoursIA (post [INFO] PRESERVATION INTEGRALE, 2026-10-08).
  2. Consolidation de la méthode durable dans la page existante de la série — c'est ce que cette PR livre désormais.

Ce que cette PR livre

docs/lean/junctions-scan-po-2024.md reçoit la section « Seconde occurrence consolidée (po-2025, 2026-10-08) » : les deux cécités d'instrument déjà documentées pour po-2024 sont confirmées sur po-2025, et une troisième leur est ajoutée, propre à l'organe dédié check_mathlib_cache.py — les jonctions pendantes y sont classées reel (retour anticipé l.88 : exists() suit le lien vers une cible absente, avant la détection de jonction l.93-96). Chiffres clés du scan po-2025 : 30 lacs portant mathlib, 18 jonctions, 0 utilisable (14 pendantes vers v4.33.0-db584cd6, 4 MISMATCH vers v4.32.1-520045ab), 1 seul checkout physique réel, 0/36 oleans atteignables — le détail intégral vit sur le dashboard, pas dans le dépôt. La proposition §4 s'élargit à quatre états (JUNCTION-OK/COLD/MISMATCH/DANGLING).

Les renvois du script et de son test vers le rapport retiré sont reroutés vers la section consolidée ; le test reçoit au passage le filet d'encodage errors="replace" (#19480).

Périmètre effectif — 3 fichiers, 15 insertions, 4 suppressions

  • docs/lean/junctions-scan-po-2024.md (+10/-0) — la section consolidée ;
  • scripts/lean/check_mathlib_cache.py (+2/-2) — docstring et commentaire : renvois reroutés ;
  • scripts/lean/tests/test_check_mathlib_cache.py (+3/-2) — renvois reroutés + filet d'encodage.

Aucun notebook, aucun workflow CI touché. Le script et son test ne changent que des commentaires/docstring et l'encodage d'un subprocess.run de fixture — aucune sémantique d'analyse modifiée.

Ce que cette PR ne fait pas

Aucun Apply n'est lancé ni proposé — ni donneur (le donneur déclaré conway_lean n'a plus de .lake/packages ; le seul checkout physique est dans un groupe isolé), ni filet (hadBackup: false, aucun .bak-2611 dans l'arbre). Le geste utile est le retrait des 18 jonctions, geste disque soumis à GO nominatif — arbitrage user ouvert côté dashboard.

See #13962
Part of #4362

🤖 Generated with Claude Code

Exception de portee (#15719)

Justification de portée (exception #15719, résidu final mesuré) : la CR 5463024284 borne elle-même le livrable à la méthode durable — la 2e occurrence a livré la 3e cécité d'instrument, une 3e occurrence n'ajouterait que du volume.

jsboige and others added 2 commits October 8, 2026 05:15
Le rapport po-2025 manquait a la serie (po-2023/2024/2026/2027 existaient
deja sur main). Mesure resolue des cibles : 18 jonctions NTFS, dont 14 vers
une cible INEXISTANTE (le groupe v4.33.0-db584cd6 est un repertoire vide) et
4 vers un store vide appartenant a une autre toolchain (cible v4.32.1-520045ab
contre lac v4.33.0 -> derive). Oleans Mathlib atteignables : 0 / 36.
Aucun .bak-2611 dans l'arbre, hadBackup:false sur les 7 membres declares ->
Rollback sans filet. Le donneur conway_lean n'a plus de .lake/packages du tout.

Le Scan rend pourtant "Economie totale potentielle : 0 GB" -- metrique aveugle
ici : elle ne compte que les checkouts physiques, donc une machine dont les 18
jonctions sont cassees recoit la meme ligne qu'une machine sans travail.

Deux angles morts d'instrument, mesures et documentes :
- setup_shared_mathlib.ps1 -Mode Scan affiche JUNCTIONED sans resoudre la
  cible, et groupe le lac par son propre lean-toolchain, pas par la cible de sa
  jonction (4 lacs listes v4.33.0 alors que leur jonction pointe v4.32.1 --
  meme angle mort que po-2027-CoursIA2 sur kelly_lean) ;
- check_mathlib_cache.py classe les jonctions PENDANTES "absent" + "reel" :
  retour anticipe l.88 (mathlib.exists() suit le lien vers une cible absente)
  avant la detection de jonction l.93-96. Path.is_junction() les voit juste.

Angle mort deja propose par junctions-scan-po-2024.md section 4, resté ouvert :
po-2025 en est la seconde occurrence.

Aucun Apply lance ni propose (ni donneur, ni sauvegarde) ; le geste utile est
le retrait des 18 jonctions, geste disque soumis a GO nominatif.

See #13962
Part of #4362

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…erential_lean

Le bloc « Portee de la mesure » borne les chiffres du resume au
2026-10-08 ~03:15Z : le `lake exe cache get` + `lake build` de
`differential_lean` tournait pendant le releve et a cree son
`.lake/packages/mathlib` a 03:24Z. Le compte « 1 checkout physique »
est donc un instantane, la ou les 18 jonctions sont stables.

See #13962
Part of #4362

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: 00c3501
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 0a07ac7150b51fe44d4fd62fee1448acb33075a159da20dc76e1cf89f80f6ca0
diff-files: 1
diff-additions: 241
diff-deletions: 0
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 3
[/ADJOINT PREFLIGHT]

jsboige and others added 3 commits October 8, 2026 10:45
Le garde docs-index-guard refuse un doc vivant inatteignable depuis
l'index ; le scan po-2025 etait livre sans sa ligne. Garde verifie
localement : 221/221 atteignables, rc=0.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot added the markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. label Oct 8, 2026
@github-actions

github-actions Bot commented Oct 8, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #19860 (Docs(13962): scan junctions po-2025 -- 18 jonctions, aucune utilisable) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

@jsboige

jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: dbd3034
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e8da3c5a099a1aca4654c0cb0bf7601b575b0e1909bb554a026ab39f4cd1db38
diff-files: 2
diff-additions: 242
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01 myia-ai-01 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

CHANGES_REQUESTED — le delta est explicitement un rapport de scan de machine et detat de flotte date (aucun script ni implementation modifiee). CLAUDE.md section A et harness-hygiene interdisent les rapports de cycle/audit dans le depot : conserver la mesure et les logs sur RooSync, et ne garder dans docs que la methode durable consolidee dans la documentation existante des jonctions. Preserver integralement les mesures avant retrait. La nouvelle page ne doit pas figer un etat local ou un GO user en documentation publique.

…24 (review 5463024284)

Le rapport junctions-scan-po-2025.md etait un scan local date sans
implémentation : mesure integrale PRESERVEE sur le dashboard RooSync
workspace-CoursIA (post [INFO] PRESERVATION INTEGRALE) AVANT retrait.
Seuls les deux angles morts + la methode durable restent dans docs,
consolides dans junctions-scan-po-2024.md §4 (seconde occurrence :
14 pendantes, classe JUNCTION-DANGLING nouvelle, cecite early-return
de check_mathlib_cache.py, protocole reparsepoint + enumeration
a travers le lien). Ligne d'index docs/README.md retiree avec le
fichier ; 3 references de commentaires (organe + tests) repointees
vers la section consolidee ; 1 subprocess text=True sans encoding=
du meme fichier passe au fix canonique (#12811). Tests organe :
35 passed.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner Author

Review 5463024284 traitee au commit 7f21a7b (tete nouvelle), point par point :

  1. Preservation avant retrait : la mesure integrale (verdict, tableaux, scan verbatim, share-state, protocole, position flotte) est posee sur le dashboard RooSync workspace-CoursIA (post [INFO] PRESERVATION INTEGRALE, horodate) AVANT la suppression du fichier -- rien n'est perdu.
  2. Consolidation dans la doc existante : les deux angles morts + la methode durable vivent desormais dans junctions-scan-po-2024.md §4, sous-section « Seconde occurrence consolidee (po-2025, 2026-10-08) » -- la proposition JUNCTION-OK/COLD/MISMATCH s'elargit a JUNCTION-DANGLING (classe nouvelle : 14 pendantes), et la cecite early-return de check_mathlib_cache.py (l.88 avant l.93-96 -> affiche 'reel') y est consignee avec l'API qui voit juste (Path.is_junction).
  3. Retrait du rapport date : junctions-scan-po-2025.md supprime, ligne d'index docs/README.md retiree avec lui, et les 3 references de commentaires qui le citaient (organe + tests, deja sur main) repointees vers la section consolidee -- aucun lien mort.
  4. Aucun retrait de jonction : confirme, aucun geste disque.

En passant, le pre-commit a refuse un subprocess text=True sans encoding= preexistant dans test_check_mathlib_cache.py:58 -- passe au fix canonique encoding="utf-8", errors="replace" (#12811). Tests de l'organe : 35 passed. Dossier tiers a suivre apres stabilisation CI.

@github-actions github-actions Bot removed the markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. label Oct 8, 2026
@github-actions

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@github-actions github-actions Bot added the trivial-diff-advisory Diff trivial : grain META mecanique sans fournee ni exception ecrite (#15740) label Oct 8, 2026
@github-actions

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 19 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19860
head: 7f21a7b
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 51ef18c2661f10a9338fc34b203466095fc3ed4effdb89a27a4da69ae21d33a0
diff-files: 3
diff-additions: 15
diff-deletions: 4
checks: latest-wins-green
b0: blocked
scope: pass
domain: not-applicable
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 3
[/ADJOINT PREFLIGHT]

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: 7f21a7b
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 922a6487aa7937f8df1634f1afe1bcffc3603141c5ec994a9a8492f26ca2736c
diff-files: 3
diff-additions: 15
diff-deletions: 4
checks: latest-wins-green
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 3
[/ADJOINT PREFLIGHT]

@jsboige jsboige changed the title Docs(13962): scan junctions po-2025 -- 18 jonctions, aucune utilisable Docs(13962): consolider le scan junctions po-2025 dans la doc existante -- 3e cecite d'instrument Oct 9, 2026
@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: 7f21a7b
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 30a56dfcc445974931e0756224759c4c2610042a17a377f9e6083ecb0ebb3058
diff-files: 3
diff-additions: 15
diff-deletions: 4
checks: latest-wins-green
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 3
[/ADJOINT PREFLIGHT]

@github-actions github-actions Bot removed the trivial-diff-advisory Diff trivial : grain META mecanique sans fournee ni exception ecrite (#15740) label Oct 9, 2026

@myia-ai-01 myia-ai-01 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ma réserve est levée : review myia-ai-01 5463024284 (CHANGES_REQUESTED, 2026-10-08), relue à la tête 7f21a7b20d.

Ce que j'ai demandé, et ce que j'ai vérifié dans le diff :

  • Pas de rapport de scan daté dans le dépôt. docs/lean/junctions-scan-po-2025.md n'est plus ajouté. La PR ne crée aucune page.

  • La méthode durable est consolidée dans la doc existante. C'est une section de 10 lignes dans junctions-scan-po-2024.md §4 :

    • la troisième cécité d'instrument, avec ses lignes de code : l.88, puis l.93-96 ;
    • la méthode de résolution de cible ;
    • les quatre états JUNCTION-OK/COLD/MISMATCH/DANGLING.

    Aucun état local n'y est figé comme vérité courante, et aucun GO user n'y figure.

  • La mesure est préservée avant le retrait. Elle a été postée sur le dashboard workspace-CoursIA, et la version v1 du fichier reste lisible au commit dbd303421e, conservé par refs/pull/19860/head. Aucun de ces deux supports ne dépend de la PR.

  • Les renvois sont reroutés. Les trois renvois à l'ancien fichier, dans la docstring, un commentaire et le test, pointent vers la section consolidée. Ce ne sont que des commentaires : aucune sémantique d'analyse ne change. Le filet encoding="utf-8", errors="replace" posé sur la fixture mklink est le correctif canonique (#12811).

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: 7f21a7b
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 2
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 00cf70ce0eea38d1367438f64aace91027e20e04a494ab42e50a41d6a8208663
diff-files: 3
diff-additions: 15
diff-deletions: 4
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 0
supersedes: 9
supersedes-why: le motif de l'ancien dossier (b0: blocked -- la CR 5463024284 d'ai-01) est eteint et mesure : ai-01 l'a levee par l'APPROVED 5469039277, le B.0 vivant rend rc=0 (mesure firsthand ce cycle par le gate lui-meme), et la tete 7f21a7b est inchangee depuis le dossier de 09:20:55Z.
[/ADJOINT PREFLIGHT]

@myia-ai-01
myia-ai-01 merged commit 4da045a into main Oct 9, 2026
45 of 55 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants